module Assignment2and3 where 

import List 
import Lexer
import Parser
import CNF
import Assignment1
import System.Random
import Test.QuickCheck
import Test.QuickCheck.Gen

main :: IO ()
main = do
  quickCheck prop_form

-- TODO this calls a function from Assignment 1 to determine if the original
--      formula and its CNF form are equivalent. Because Assignment 1 is not
--      yet done this will not yet produce the correct results.
prop_form :: Form -> Bool
prop_form f = logicalEquivalence f (conv f)

-- Generates a random formula. There is bias towards generating proposition 
-- letters, so that the generated formulas don't become too long.
instance Arbitrary Form where
  arbitrary = frequency [(8,return arbitraryProp),
                         (2,return (Neg (fromGen arbitrary))),
                         (2,return (Cnj [fromGen arbitrary, fromGen arbitrary])),
                         (2,return (Dsj [fromGen arbitrary, fromGen arbitrary])),
                         (1,return (Impl (fromGen arbitrary) (fromGen arbitrary))),
                         (1,return (Equiv (fromGen arbitrary) (fromGen arbitrary)))]

-- Generates a random proposition letter. This is limited to the range 1..5,
-- to prevent truth tables from becoming too long.
arbitraryProp :: Form
arbitraryProp = Prop (fromGen (choose (1,5)))

-- TODO what we're trying to do is get something from the generator. However, 
--      this requires a StdGen, and the only StdGen that can be used without
--      the IO monad isn't really that random. So, we get results of 2 2 2 2,
--      or --------2, etc.
fromGen :: Gen a -> a
fromGen a = unGen a (mkStdGen 42) 1
